perm filename NSF.80[E80,JMC] blob
sn#544043 filedate 1980-10-29 generic text, type C, neo UTF8
COMMENT ⊗ VALID 00010 PAGES
C REC PAGE DESCRIPTION
C00001 00001
C00002 00002 .device XGP
C00005 00003 .onecol BEGIN "TITLE PAGE"
C00006 00004 .BEGIN "COVER PAGE"
C00009 00005 .EVERY HEADING(%3{SECNAME},{SSNAME},{PAGE!}) page←0 twocol cb Abstract
C00020 00006 .cb Recent Advances and Changes in Direction of the Research
C00033 00007 .cb Organization of the work
C00035 00008 .cb Personnel
C00045 00009 .onecol cb Budget
C00055 00010 .twocol bib
C00060 ENDMK
C⊗;
.device XGP;
.turn on "α%";
.font 1 "baxl30"; font 2 "baxm30"; font 3 "baxb30"; font 4 "baxs30";
. << output a ligature & restore fonts >>
.recursive macro lig(A); ⊂start f_f←thisfont; ("%*%4αA%*%"&f_f) end⊃;
.
.AT "ff" ⊂ IF THISFONT=1 THEN lig(@) ELSE if thisfont=2 then lig(P)
. else if thisfont=3 then lig("`") else "fαf" ⊃;
.AT "ffi" ⊂ IF THISFONT=1 THEN lig(A) ELSE if thisfont=2 then lig(Q)
. else if thisfont=3 then lig(a) else "fαfαi" ⊃;
.AT "ffl" ⊂ IF THISFONT=1 THEN lig(B) ELSE if thisfont=2 then lig(R)
. else if thisfont=3 then lig("b") else "fαfαl" ⊃;
.AT "fi" ⊂ IF THISFONT=1 THEN lig(C) ELSE if thisfont=2 then lig(S)
. else if thisfont=3 then lig(c) else "fαi" ⊃;
.AT "fl" ⊂ IF THISFONT=1 THEN lig(D) ELSE if thisfont=2 then lig(T)
. else if thisfont=3 then lig(d) else "fαl" ⊃;
.AT "--" ⊂ IF THISFONT=1 THEN lig(E) ELSE if thisfont=2 then lig(U)
. else if thisfont=3 then lig(e) else "α-α-" ⊃;
.font 5 "gacs25";
.font 6 "clar30"
.font 9 "sail25"
.sides←1;
.require "twocol.pub[sub,sys]" source_file;
.MACRO YON(LBL) ⊂ "Section "; SUB2! LBL ⊃;
.MACRO BC ⊂ BEGIN PREFACE 0; INDENT 1,4; CRBREAK nojust ⊃
.MACRO BS ⊂ BEGIN PREFACE 0; INDENT 1,4; nojust ⊃
.MACRO SUB(IND) ⊂ INDENT 0,IND; TABS IND+1;⊃
.MACRO IB ⊂ turn on "%";
.AT """" ⊂ (IF THISFONT=1 THEN "%3" ELSE "%1"); ⊃
.AT "<" ⊂ "%2" ⊃; AT ">" ⊂ "%1" ⊃;
. ⊃
.MACRO BIB ⊂ CB(References);
. BEGIN INDENT 0,3; NOJUST; IB;
. AT "AIM-" ⊂ "Stanford AI Memo AαIαMα-" ⊃;
. COUNT exref TO 200
. AT "⊗" ⊂ IF LINES<3 THEN NEXT COLUMN; NEXT EXREF; ("["&EXREF&"] ") ⊃
. ⊃
.
.COUNT ITEM
.AT "#" ⊂NEXT ITEM;(ITEM!);⊃;
.SECNAME←"";
.portion some; place text;
.every heading();
.onecol; BEGIN "TITLE PAGE"
.SKIP TO COLUMN 1;
.CENTER;
.PREFACE 0;
.SELECT 1;
Research Proposal Submitted to
.SKIP 2;
%3THE NATIONAL SCIENCE FOUNDATION
.SKIP 2;
%1for
.SKIP 2;
%3Basic Research in Artificial Intelligence
.SKIP 2;
%1by
.SKIP 2;
John McCarthy
Professor of Computer Science
Principal Investigator
.SKIP 8;
October 1980
.SKIP 5;
Computer Science Department
.SKIP 1;
%3STANFORD UNIVERSITY
.SKIP 1;
%1Stanford, California
.END "TITLE PAGE";
.BEGIN "COVER PAGE"
.SKIP TO COLUMN 1;
.NOFILL;
.PREFACE 0;
.INDENT 0,0,0;
.SELECT 1;
.TURN ON "\↓_";
.AT "≤≤" TXT "≥" ⊂ }↓_%9TXT%*_↓{ ⊃;
. BEGIN "COVER PAGE TITLE"
. CENTER;
. SELECT 6;
Research Proposal Submitted to the National Science Foundation
. END "COVER PAGE TITLE";
.SKIP 5;
.SELECT 1;
Proposed Amount ≤≤$417,592≥. Proposed Starting Date ≤≤1 July 1981≥. Proposed Duration ≤≤3 years≥.
.SKIP 3;
Title ≤≤Basic Research in Artificial Intelligence≥
.TABS 40;
.SKIP 3;
Principal Investigator ≤≤John McCarthy≥\Submitting Institution ≤≤Stanford University≥
Soc. Sec. No. ≤≤558-30-4793≥\Department ≤≤ Computer Science ≥
\Address ≤≤Stanford, California 94305≥
.SKIP 3;
Make grant to ≤≤Board of Trustees of the Leland Stanford Junior University≥
.SKIP 3;
Endorsements:
.TABS 10,34,57;
.SKIP 1;
\Principal Investigator\Department Head\Institutional Admin. Official
.TABS 10,34,58;
.PREFACE 1;
Name\≤≤John McCarthy ≥\≤≤Jeffrey D. Ullman≥\≤≤ ≥
.SKIP 1;
Signature\≤≤ ≥\≤≤ ≥\≤≤ ≥
Title\≤≤Professor ≥\≤≤Professor & Acting Chairman ≥\≤≤ ≥
Telephone\≤≤(415) 497-4430 ≥\≤≤(415) 497-4079 ≥\≤≤ ≥
Date\≤≤ ≥\≤≤ ≥\≤≤ ≥
.END "COVER PAGE";
.EVERY HEADING(%3{SECNAME},{SSNAME},{PAGE!}); page←0; twocol; cb Abstract
.fill adjust
This is a request for a grant of $417,592
for continued support of basic research in artificial intelligence
with emphasis on the structure of formal reasoning, epistemological
problems of artificial intelligence and mathematical theory of computation.
The mathematical theory of computation supports the AI work by
providing tools for reasoning about complex strategies and
showing that they attain their goals.
The line of research being pursued was already outlined in our 1977
proposal, and this proposal incorporates much material from that one.
.cb Epistemological Problems of Artificial Intelligence
Artificial intelligence has proved to be a difficult branch
of science. Some people thought that human-level intelligence
could be achieved in ten or twenty years, but such estimates were based on
the difficulties they could see when they made the optimistic
predictions. Our opinion is that major scientific discoveries
are required before human-level general intelligence can be reached.
Moreover, many of these discoveries require theoretical advances and
not merely extending current ideas for producing "expert programs"
to new domains.
The recent emphasis by ARPA and other agencies sponsoring AI
research on immediate applications has resulted in a serious
imbalance. Deciding what the basic issues are is difficult
enough without having to formulate everything in terms of demonstration
programs to be available in two years. While there has been some
recent increase in understanding of the need for basic research,
especially since 1978,
the main interest is still on short term goals.
Our research is based on the idea that, for many purposes,
the problems of artificial intelligence can be separated into two
parts - an epistemological part and a heuristic part.
The %2epistemological%1 part concerns what facts and inference
rules are available for solving a problem and how they can be
represented in the memory of a computer, and the heuristic part
concerns procedures for deciding what to do on the basis of the
necessary facts. Most work in AI has concerned %2heuristics%1,
and computer representations of information have been chosen that
are capable of representing only a part of the information that
would be available to a human. The modes of reasoning used by
present programs are often even weaker than the representations
themselves.
The lines of research we plan to pursue are exemplified in
the attached papers (McCarthy 1979a,b,1980).
Here we shall explain how this work fits together. Our long range goal is
a program that can be told facts about the world and can use them
effectively to achieve the goals it is given.
Sometimes it will use the facts directly from its data base using
deductive and inductive processes like the deductive processes
of mathematical logic. However, we are already sure, (McCarthy 1980),
that conjectural processes will be needed that go beyond deduction
as presently conceived. Sometimes it will use these facts to compile
"expert programs" that use these facts in a more efficient way than
simple reasoning. However, the expert programs will have to defer
to reasoning when unexpected use of the factual data-base is required.
We do not propose to implement such a program immediately -
maybe not within the next five years. This is because its
success depends on successful formalization of facts about the world.
We have made progress in this formalization, but we may be occupied
with it exclusively for the forseeable future. In short we will
emphasize theoretical artificial intelligence except for some work
with proof-checkers.
The main areas of our previous accomplishment and future work
are the following (as now seen):
.item← 0
#. Development of %2circumscription%1 as a mode of reasoning and its
application to artificial intelligence. %2Circumscription%1 formalizes
the process of concluding (often incorrectly) that a certain collection
of facts is all that are relevant for solving a problem. It does this
by allowing one to formally assume that the entities that are generated
by specified processes are all the entities of a specified kind.
This is common in human reasoning and, for reasons described in
(McCarthy 1980), cannot be accomplished by any form of deduction.
#. Treating concepts as objects. This, described in
(McCarthy 1979a), facilitates, and may be required for, reasoning about
knowledge, belief, wants, possibility and necessity.
As we shall explain later, it may be necessary to replace the approach
of that paper by one which makes distinctions of language between objects and
and concepts of them only when required. Not making the distinctions
would be accomplished by some kind of non-monotonic reasoning.
#. The current biggest gap in computer reasoning about the physical world
is the complete lack of a system for reasoning with partial
information about concurrent processes.
All the current problem solving programs assume that each action of the
program produces a next state that depends on the current state, the action,
and sometimes on a random variable. They don't take into account continuous
processes or the fact that other actions and events may be taking place.
We believe that circumscription may be important in formalizing what
people know about such processes.
Little progress has been made by anyone on this problem in the last few
years.
#. We also plan some study of the theory of patterns, especially higher
order patterns in which function variables may be matched and relations
between patterns - for example, the relation between a pattern describing
a type of three-dimensional object such as a person or a vehicle and its
patterns of its perception - such as its projection on a retina as modified
by angle of vision, lighting and occlusion by other objects.
In all this work, the emphasis is on representation of the information
that is actually available to a person or robot with given opportunities to
observe and compute and act.
Besides the work on artificial intelligence, McCarthy has been
studying various methods for proving programs correct. In the last
few years, an approach called Elephant has been developed that involves
representing program variables as functions of time. This complements
the approach of (McCarthy and Cartwright 1979c).
.cb Recent Advances and Changes in Direction of the Research
Since our 1977 proposal, interest has increased in non-monotonic
reasoning. We organized a mini-conference at Stanford in 1978, and
that led to a special issue of %2Artificial Intelligence%1 containing
updated versions of the papers presented at the conference together
with a paper by Raymond Reiter (1980). Drew McDermott and Jon Doyle
have attacked the problem through what they call %2non-monotonic logic%1
and Raymond Reiter has introduced a %2logic of defaults%1. Our own
approach through circumscription has been further developed in
the published version.
Participation in the study on artificial intelligence and
philosophy held in 1979-80 at the Center for Advanced Study in
Behavioral Sciences has produced somewhat of change in viewpoint
although not yet to definite technical results. Consider the
following problem:
%2Suppose that a law making it a crime to "attempt to bribe
a public official" has been passed, and suppose further that the
law has been enforced with various trials, convictions and appeals
for 20 years before the following questions arise.
(1) Person A attempts to bribe B to help him get a contract
under the impression that B is a private consultant to a government agency.
In fact, B is an official of the agency. A offers the defense that
since he didn't know B was a public official, he couldn't have been
attempting to bribe a public official.
(2) C attempts to bribe D, but D had resigned his position
as a public official before the attempt was made. The defense is
offered that attempting to bribe someone who in fact is not a
public official isn't attempting to bribe a public official.
(3) E lets it be known around town that he will pay $1,000
to any public official who can fix his drunk driving conviction.
There happens to be no official who can fix the conviction. Is
E guilty of attempting to bribe a public official if he isn't
attempting to bribe a specific person? Is it relevant whether there
is a person who can do what E wants done%1?
Such questions are familiar to both philosophers
and lawyers. The distinction between (1) and (2) is the
well known %2de re - de dicto%1 distinction between interpretations
of "attempting to bribe a public official". This distinction and
even more complicated distinctions have been made in court decisions.
A famous 1879 case concerns a cow which was bought on the basis
that the seller thought the cow was infertile and the buyer thought
he could make the cow breed. When he discovered that the cow was
actually pregnant, the seller refused to deliver on the grounds that
he had sold a barren cow. The issue is whether there was a meeting
of minds.
When we try to design an AI system, our interest in such
problems is different from that expressed by either philosophers
or lawyers.
They are interested in making distinctions that have not previously
been made. The primary AI interest should be in the state of mind
of the lawyer or judge who tries cases of attempting to bribe a
public official for twenty years without ever thinking of the
distinction. When the distinction is pointed out, he can understand
that there is a distinction, although he may not have any definite
way of resolving the ambiguity in the law.
(McCarthy 1979a) presents a formalism that resolves simple
forms of %2de re - de dicto%1 distinction, and we knew about
the problem of stating that John is seeking a unicorn without
presuming the existence of unicorns and planned to resolve it.
The formalism of that paper allowed both physical entities and
concepts of them to be individuals in a first order theory.
All statements of knowing or wanting or attempting take concepts
of objects, and the %2de re%1 and %2de dicto%1 versions of "attempting
to bribe a public official" would have different forms, and if
the legislature wrote the law in the language of (McCarthy 1979a),
they would automatically say one or the other or the conjunction
or the disjunction.
However, it now seems that philosophers and lawyers invent
new distinctions all the time, and we certainly can't revise the
foundation of our language every time such a distinction comes
along. Even if we could, the question still arises of what
was the meaning of what was said before the distinction was
made.
While it is possible that the formalism of (McCarthy 1979a)
could be extended to
cover all cases of interest, this now seems unlikely, and it
is interesting to explore a different approach. This new approach
has other advantages as well.
The idea is complicated and not well developed, but here is a
preliminary version.
We still use a first order system, but we have only one
form of expression. We have the default rule that equals may
be substituted for equals unless there is a reason why not. In
philosopher's Latin, %2Ceteris paribus, de re = de dicto%1. Our
hope is that extending non-monotonic reasoning to say that certain
concepts are not ambiguous unless there is reason to the contrary
will allow AI systems that behave more like people in that respect.
The philosophers have a slogan that doing philosophy should
not depend on doing all science first. Thus understanding what
people mean by the word "fish" should not depend on the philosopher
knowing what distinguishes fish from other vertebrates. It appears
that we need another slogan to the effect that doing AI should
not depend on doing all philosophy first. Thus it should be possible
to design a program that could discuss cases of attempting to
bribe a public official without the programmer knowing about
the ambiguous cases. The program he creates, like the programmer
himself, should be able to understand the distinction when it is
pointed out but needn't have any automatic way of resolving
the doubtful cases.
We have some examples of using circumscription for this
in a second order formalism. Namely, a suitable circumscription
formula asserts that a function like %2Telephone%1 of (McCarthy 1979a)
is extensional unless there is a reason why not. However, this
is may not be a sufficiently general way of treating the problem.
McCarthy and interested students will explore this problem
in the next three years.
Much of the research has involved using our interactive
proof-checker and theorem prover for first order logic. Work on
FOL is now being supported under a different NSF grant. Besides
FOL, Jussi Ketonen is now developing from scratch a new proof
checker caled EKL incorporating the lessons of FOL that will hopefully be
be suited for checking the proofs of substantial mathematical
theorems. Separate support is being solicited for that work, but
McCarthy's participation in helping plan and apply EKL is part of
this proposal.
The use of proof-checkers in this research is exemplified
by Filman's (1979) thesis. Unlike mathematical reasoning, much
common sense reasoning uses observation as well as explicitly
given premisses. Filman used FOL to show that the
reasoning involved in the solution of a hard retrospective chess problem
can be formalized in first order logic supplemented by the ability to
observe a chess board.
the semantic attachment
mechanism of FOL was used to build a simulation of his chess world. He
could then use the semantic simplification routines of FOL to answer (in a
single step) questions like "is the black king in check on board B" by
looking at the model rather than deducing from axioms giving the
positions of the pieces and others about the rules of
chess that black was in check. This single use of semantic attachment
saves several hundred steps over traditional formalizations.
Filman's
proof is still much longer than the informal proof, showing that we still
don't fully understand how humans combine observation with deduction.
Filman is now at the University of Indiana, but we are trying to
develop a new approach to combining observation and deduction before
starting another proof of this kind.
.cb Organization of the work
The work will be done by John McCarthy and interested graduate
students.
Graduate students help with implementations
and pursue thesis research in artificial intelligence (concentrating
on epistemological problems) and in mathematical theory of computation.
The group shares interests with the separately supported groups in
mathematical theory of computation and theorem proving.
.cb Facilities
The project will be part of the Stanford University Artificial
Intelligence Laboratory and will use its computer facilities which have
now been merged with the facilities of the Computer Science Department
for accounting purposes.
The Laboratory is directed by John McCarthy and has been mainly supported
by ARPA in the past, but the fraction of its support provided by ARPA
is diminishing.
.cb Personnel
.cb Biography of John McCarthy
.begin nojust; indent 0,4;
BORN: September 4, 1927 in Boston, Massachusetts
EDUCATION:
.preface 0; crbreak;
B.S. (Mathematics) California Institute of Technology, 1948.
Ph.D. (Mathematics) Princeton University, 1951.
.skip
HONORS AND SOCIETIES:
American Mathematical Society,
Association for Computing Machinery,
Sigma Xi,
Sloan Fellow in Physical Science (1957-59),
ACM National Lecturer (1961),
Sigma Xi National Lecturer (1978),
IEEE,
A.M. Turing Award from Association for Computing Machinery (1971).
.skip
PROFESSIONAL EXPERIENCE:
Proctor Fellow, Princeton University (1950-51),
Higgins Research Instructor in Mathematics, Princeton University (1951-53),
Acting Assistant Professor of Mathematics, Stanford University (1953-55),
Assistant Professor of Mathematics, Dartmouth College (1955-58),
Assistant Professor of Communication Science, M.I.T. (1958-61),
Associate Professor of Communication Science, M.I.T. (1961-62),
Professor of Computer Science Stanford University (1962 - present).
.skip
PROFESSIONAL RESPONSIBILITIES AND SCIENTIFIC INTERESTS:
.crspace;
With Marvin Minsky organized and directed the Artificial Intelligence
Project at M.I.T.
Organized and directs Stanford Artificial Intelligence Laboratory.
Originated the LISP programming system for computing with
symbolic expressions, participated in the development
of the ALGOL 58 and the ALGOL 60 languages.
Present scientific work is in the fields of Artificial
Intelligence, Computation with Symbolic Expressions,
Mathematical Theory of Computation, Time-Sharing computer
systems.
SELECTED PUBLICATIONS:
.count ref inline; at "⊗" ⊂next ref; ("["&ref&"] ");⊃
. at "<" ⊂"%2"⊃; at ">" ⊂"%1"⊃;
⊗"Towards a Mathematical Theory of Computation", in
<Proc. IFIP Congress 62>, North-Holland, Amsterdam, 1963.
⊗"A Basis for a Mathematical Theory of Computation",
in P. Braffort and D. Hershberg (eds.), <Computer Programming and
Formal Systems>, North-Holland, Amsterdam, 1963.
⊗(with S. Boilen, E. Fredkin, J.C.R. Licklider)
"A Time-Sharing Debugging System for a Small Computer", <Proc.
AFIPS Conf.> (SJCC), Vol. 23, 1963.
⊗(with F. Corbato, M. Daggett) "The Linking
Segment Subprogram Language and Linking Loader Programming
Languages", <Comm. ACM>, July 1963.
⊗"Problems in the Theory of Computation", <Proc. IFIP
Congress 1965>.
⊗"Time-Sharing Computer Systems", in W. Orr (ed.),
<Conversational Computers>, Wiley, 1966.
⊗"A Formal Description of a Subset of Algol", in T.
Steele (ed.), <Formal Language Description Languages for Computer
Programming>, North-Holland, Amsterdam, 1966.
⊗"Information", <Scientific American>, September
1966.
⊗"Computer Control of a Hand and Eye", in <Proc.
Third All-Union Conference on Automatic Control (Technical
Cybernetics)>, Nauka, Moscow, 1967 (Russian).
⊗(with D. Brian, G. Feldman, and J. Allen) "THOR -- A
Display Based Time-Sharing System", <Proc. AFIPS Conf.> (FJCC), Vol.
30, Thompson, Washington, D.C., 1967.
⊗(with James Painter) "Correctness of a Compiler for
Arithmetic Expressions", Amer. Math. Soc., <Proc. Symposia in
Applied Math., Math. Aspects of Computer Science>, New York, 1967.
⊗"Programs with Common Sense", in Marvin Minsky
(ed.), <Semantic Information Processing>, MIT Press, Cambridge, 1968.
⊗(with Lester Earnest, D. Raj. Reddy, Pierre Vicens) "A
Computer with Hands, Eyes, and Ears", <Proc. AFIPS Conf.> (FJCC),
1968.
⊗(with Patrick Hayes) "Some Philosophical Problems from the
Standpoint of Artificial Intelligence", in Donald Michie (ed.),
<Machine Intelligence 4>, American Elsevier, New York, 1969.
⊗"The Home Information Terminal", <Man and Computer,
Proc. Int. Conf., Bordeaux, 1970>, S. Karger, New York, 1972.
⊗"Mechanical Servants for Mankind," in <Britannica Yearbook of
Science and the Future>, 1973.
⊗Book Review: "Artificial Intelligence: A General Survey" by Sir James
Lighthill, in <Artificial Intelligence, Vol. 5, No. 3>, Fall 1974.
⊗"Modeling Our Minds" in <Science Year 1975>, The World Book Science
Annual, Field Enterprises Educational Corporation, Chicago, 1974.
⊗"The Home Information Terminal," invited presentation, AAAS Annual
Meeting, Feb. 18-24, 1976, Boston.
⊗"An Unreasonable Book," a review of <Computer Power and Human Reason>,
by Joseph Weizenbaum (W.H. Freeman and Co., San Francisco, 1976)
in SIGART Newsletter #58, June 1976, also in <Creative Computing>,
Chestnut Hill, Massachusetts, 1976 and in "Three Reviews of
J. Weizenbaum's <Computer Power and Human Reason>, (with B. Buchanan
and J. Lederberg), Stanford Artificial Intelligence Laboratory
Memo 291, Computer Science Department, Stanford, November 1976.
⊗Review: <Computer Power and Human Reason>, by Joseph Weizenbaum (W.H.
Freeman and Co., San Francisco, 1976) in Physics Today, 1977.
⊗"The Home Information Terminal" to appear in The Grolier Encyclopedia,
1977, also to appear in <The International YearBook and Statemen's Who's
Who>, Surrey, England, 1977.
⊗"Dialnet and Home Computers" (with Les Earnest), <Proceedings of the
First West Coast Computer Faire and Conference>, San Francisco, April 1977.
⊗"On The Model Theory of Knowledge" (with M. Sato, S. Igarashi, and
T. Hayashi), <Proceedings of the Fifth International
Joint Conference on Artificial Intelligence>, M.I.T, Cambridge, 1977.
⊗"Another SAMEFRINGE", in SIGART Newsletter No. 61, February 1977.
⊗"Ascribing Mental Qualities to Machines" to appear in <Essays in Philosophy
and Computer Technology>, National Symposium for Philosophy and Computer
Technology, New York, 1977.
⊗"Epistemological Problems of Artificial Intelligence", <Proceedings of the Fifth
International Joint Conference on Artificial Intelligence>, M.I.T., Cambridge, 1977.
(Additional McCarthy papers are listed in the references at the end of
this proposal).
.end
.onecol; cb Budget
.begin "budget" verbatim select 5;
PERIOD COVERED: 3 Years: 1 June 1978 through 31 December 1981.
Dates: 6/1/78-5/31/79 6/1/79-5/31/80 6/1/80-5/31/81
Person- Person- Person-
A. SALARIES AND WAGES months months months
1. Senior Personnel:
a. John McCarthy, 24,257. 6.5 27,007. 6.5 29,168. 6.5
Professor
Summer 75%(2 mos.)
Acad. Yr. 50%
2. Other Personnel
a. Student Research
Assistants
(50% Acad.Yr.;
100% Summer)
(1) 7,155. 7.5 7,704. 7.5 8,320. 7.5
(2) 7,155. 7.5 7,704. 7.5 8,320. 7.5
b. Support Personnel
(1) Sec'y (20%) 2,092. 2.4 2,259. 2.4 2,440. 2.4
(2) Sys.Prog.(15%) 2,937. 1.8 3,172. 1.8 3,426. 1.8
_______ _______ _______
Total Salaries & Wages 43,596. 47,846. 51,674.
B. STAFF BENEFITS
9/1/77-8/31/78:19.0%
9/1/78-8/31/79:20.3%
9/1/79-8/31/80;21.6%
9/1/80-8/31/81;22.4%
8,708. 10,179. 11,472.
_______ ________ ________
C. TOTAL SALARIES, WAGES,
AND STAFF BENEFITS 52,304. 58,025. 63,146.
.next page
D. PERMANENT EQUIPMENT 5,000 -- --
(2 Datamedia terminals)
E. EXPENDABLE SUPPLIES 1,632. 1,730. 1,834.
& EQUIPMENT(e.g.,copying,
office supplies, postage,
freight, consulting,
honoraria)
F. TRAVEL 1,840. 1,950. 2,067.
All Domestic Travel
G. PUBLICATIONS 1,000. 1,060. 1,124.
H. OTHER COSTS 6,640. 7,038. 7,460.
1.Communication 1,600.
(telephone)
2. Computer 5,040.
Equip. Maint.
_______ ________ _______
I. TOTAL COSTS 68,416. 69,803. 75,631.
(A through H)
J. INDIRECT COSTS:58% of 36,781. 40,486. 43,866.
A through H, less D. ________ ________ ________
K. TOTAL COSTS 105,197. 110,289. 119,497.
L. THREE YEAR TOTAL 334,983.
.end "budget"
.twocol; bib;
%3Boyer, R.S., and Moore, J.S.%1 (1975) Proving Theorems About LISP Functions,
JACM Vol 22. No. 1 pp. 129-144. New York: ACM.
%3Filman, R.E.%1 (1979) The Interaction of Observation and Inference.
(AIM-327) Stanford University.
%3McCarthy, J. and Painter, J.%1 (1967) Correctness of a Compiler for
Arithmetic Expressions. %2Proc. Symposia in Applied Math., Math. Aspects
of Computer Science%1 New York: Amer. Math. Soc..
%3McCarthy, J. and Hayes, P.J.%1 (1969) Some Philosophical Problems from
the Standpoint of Artificial Intelligence. %2Machine Intelligence 4%1,
pp. 463-502 (eds Meltzer, B. and Michie, D.). Edinburgh: Edinburgh
University Press.
%3McCarthy, J.%1 (1979a) First Order Theories of Individual Concepts and
Propositions. %2Machine Intelligence 9%1, (Ed., Michie, D.). Edinburgh,
Edinburgh University Press.
%3McCarthy, J.%1 (1979b) Ascribing Mental Qualities to Machines.
%2Philosophical Perspectives in Artificial Intelligence%1, (Ed., Ringle, M.).
Harvester Press.
%3Cartwright, Robert and McCarthy, John%1 (1979c) Recursive Programs as
Functions in a First Order Theory. %2Proceedings of the International Conference
on Mathematical Studies of Information Processing%1, Kyoto, Japan.
%3McCarthy, J.%1 (1980) Circumscription - A Form of Non-Monotonic Reasoning.
%2Artificial Intelligence%1, Volume l3, Numbers l, 2, April.
%3McCarthy, J., Sato, M., Hayashi, T. and Igarashi, S.%1 (1977e)
On the Model Theory of Knowledge. Presented at %2IJCAI-1977%1;
to appear in the %2SIGART Newsletter%1.
%3Moore, Robert C.%1 (1980) Reasoning about Knowledge and Action. SRI
Artificial Intelligence Center, Technical Note 191%1, SRI International,
Menlo Park, California.
%3Sato, M.%1 (1977) A study of Kripke-type Models for some Model Logics
by Gentzen's Sequential Method, (to appear in Publ. R.I.M.S., Kyoto University).
%3Wagner, Todd J.%1 (1977) Hardware Verification. Ph.D. thesis, Stanford
University. Available as α<Arpanet:SAILα> THESIS.PUB[THE,TJW].
.end